Nuprl Lemma : es-le-interface-le
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top),
e
:E. (
(
e
le(
X
)))
le(
X
)(
e
)
loc
e
latex
Definitions
Top
,
(
e
<loc
e'
)
,
X
(
e
)
,
A
,
e
X
,
E(
X
)
,
le(
X
)
,
t
T
,
s
=
t
,
P
Q
,
P
&
Q
,
x
:
A
B
(
x
)
,
E
,
AbsInterface(
A
)
,
ES
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
e
loc
e'
,
b
Lemmas
es-le-interface
wf
,
es-E-interface
wf
,
es-is-interface
wf
,
assert
wf
,
es-le
wf
,
es-E
wf
,
top
wf
,
es-interface
wf
,
event
system
wf
,
es-le-interface-val
origin
es:ES, X:AbsInterface(Top), e:E. (
(e 
le(X))) 
le(X)(e) 
loc e es:ES, X:AbsInterface(Top), e:E. ((e le(X))) le(X)(e) loc e 
A X T Q
B(x)x:A. B(x)
B(x)loc e' b